*****ASSUME A(RW,w,W2,1)∧color(W2,w)=B;

1 A(RW,w,W2,1)∧color(W2,w)=B  (1)

*****∀E elwek3 RW,w;

2 A(RW,w,W2,1)≡(A(RW,w,W2,0)∧A(RW,w,W12,1))  

*****∀E elwek1 w;

3 A(RW,w,W12,1)≡(A(RW,w,W12,0)∧((∀w.(A(w,w1,W1,0)⊃∀w2.(A(w1,w2,W2,0)⊃color(W2,w2)=color(W2,w1)))∨∀w.(A(w,w1,W1,0%
)⊃∃w2.(A(w1,w2,W2,0)∧¬(color(W2,w2)=color(W2,w1)))))∧(∀w.(A(w,w1,W2,0)⊃∀w2.(A(w1,w2,W1,0)⊃color(W1,w2)=color(W1,%
w1)))∨∀w.(A(w,w1,W2,0)⊃∃w2.(A(w1,w2,W1,0)∧¬(color(W1,w2)=color(W1,w1)))))))  

*****TAUT A(RW,w,W12,0) 1:3;

4 A(RW,w,W12,0)  (1)

*****TAUT ∀w.(A(w,w1,W2,0)⊃∀w2.(A(w1,w2,W1,0)⊃color(W1,w2)=color(W1,w1)))∨∀w.(A(w,w1,W2,0)⊃∃w2.(A(w1,w2,W1,0)∧¬(%
color(W1,w2)=color(W1,w1)))) 1:3;

5 ∀w.(A(w,w1,W2,0)⊃∀w2.(A(w1,w2,W1,0)⊃color(W1,w2)=color(W1,w1)))∨∀w.(A(w,w1,W2,0)⊃∃w2.(A(w1,w2,W1,0)∧¬(color(W1%
,w2)=color(W1,w1))))  (1)